#LyX 2.3 created this file. For more info see http://www.lyx.org/
\lyxformat 544
\begin_document
\begin_header
\save_transient_properties true
\origin unavailable
\textclass memoir
\options openany
\use_default_options false
\maintain_unincluded_children false
\language portuguese
\language_package default
\inputencoding utf8x
\fontencoding T1
\font_roman "default" "default"
\font_sans "default" "default"
\font_typewriter "default" "default"
\font_math "auto" "auto"
\font_default_family default
\use_non_tex_fonts false
\font_sc false
\font_osf false
\font_sf_scale 100 100
\font_tt_scale 100 100
\use_microtype false
\use_dash_ligatures true
\graphics default
\default_output_format default
\output_sync 0
\bibtex_command default
\index_command default
\paperfontsize 11
\spacing single
\use_hyperref false
\papersize default
\use_geometry false
\use_package amsmath 1
\use_package amssymb 0
\use_package cancel 0
\use_package esint 1
\use_package mathdots 0
\use_package mathtools 0
\use_package mhchem 0
\use_package stackrel 0
\use_package stmaryrd 0
\use_package undertilde 0
\cite_engine basic
\cite_engine_type default
\biblio_style plain
\use_bibtopic false
\use_indices false
\paperorientation portrait
\suppress_date false
\justification true
\use_refstyle 0
\use_minted 0
\index Index
\shortcut idx
\color #008000
\end_index
\secnumdepth 3
\tocdepth 3
\paragraph_separation indent
\paragraph_indentation default
\is_math_indent 0
\math_numbering_side default
\quotes_style french
\dynamic_quotes 0
\papercolumns 1
\papersides 1
\paperpagestyle default
\tracking_changes false
\output_changes false
\html_math_output 0
\html_css_as_file 0
\html_be_strict false
\end_header

\begin_body

\begin_layout Chapter
Prefácio
\end_layout

\begin_layout Standard
Como o título indica, este livro é um manual sobre lógica formal.
 Lógica formal ocupa-se com o estudo de um certo tipo de linguagem que,
 semelhante a qualquer linguagem, pode expressar estados de coisas [
\shape italic
states of affairs
\shape default
].
 É uma linguagem formal, ou seja, suas expressões (tais como sentenças)
 são definidas formalmente.
 Isto torna-a uma linguagem muito útil, pois ela é bastante precisa sobre
 os estados de coisas que as sentenças dela descrevem.
 Em particular, na lógica formal é impossível ser ambíguo.
 O estudo dessas linguagens centram-se nas relações de acarretamento [
\shape italic
entailment
\shape default
] entre sentenças, isto é, quais sentenças se seguem de quais outras sentenças.
 Acarretamento [
\shape italic
entailment
\shape default
] é central, porque, ao entendê-lo melhor, podemos dizer quando alguns estados
 de coisas [
\shape italic
states of affairs
\shape default
] devem ocorrer, uma vez que outros estados de coisas [
\shape italic
states of affairs
\shape default
] ocorrem.
 Mas acarretamento [
\shape italic
entailment
\shape default
] não é a única noção importante.
 Também consideraremos a relação de ser satisfatível, ou seja, de não ser
 mutuamente contraditório.
 Essas noções podem ser definidas semanticamente, usando definições precisas
 de acarretamento baseadas em interpretações da linguagem — ou em teoria
 da prova [
\shape italic
proof-theoretically
\shape default
], usando sistemas formais de dedução.
\end_layout

\begin_layout Standard
Lógica formal é, obviamente, uma subdisciplina central da filosofia, na
 qual a relação lógica entre suposições [
\shape italic
assumptions
\shape default
] e as conclusões alcançadas a partir daquelas [suposições] é importante.
 Filósofos investigam as consequências de definições e suposições e avaliam
 estas definições e suposições em base das suas consequências.
 Ela também é importante na matemática e ciência da computação.
 Na matemática, linguagens formais são usadas para descrever não estados
 de coisas 
\begin_inset Quotes fls
\end_inset

cotidianos
\begin_inset Quotes frs
\end_inset

, mas sim estados de coisas matemáticos.
 Matemáticos também estão interessados nas consequências de definições e
 suposições e para eles é igualmente importante estabelecer essas consequências
 (que eles chamam 
\begin_inset Quotes fls
\end_inset

teoremas
\begin_inset Quotes frs
\end_inset

), usando métodos completamente precisos e rigorosos.
 Lógica formal fornece tais métodos.
 Na ciência da computação, lógica formal é aplicada para descrever o estado
 e os procedimentos de sistemas computacionais, por exemplo, circuitos,
 programas, base de dados etc.
 Os métodos da lógica formal podem ser similarmente usados para estabelecer
 consequências de tais descrições, tais como se um circuito é livre de erro,
 se um programa faz o que é pretendido o que ele faça, se uma base de dados
 é consistente ou se algo é verdadeiro dos dados nela.
\end_layout

\begin_layout Standard
O livro está dividido em nove partes.
 A Parte
\begin_inset space ~
\end_inset


\begin_inset CommandInset ref
LatexCommand ref
reference "ch.intro"
plural "false"
caps "false"
noprefix "false"

\end_inset

 introduz o tópico e as noções de lógica de maneira informal, sem introduzir
 uma linguagem formal ainda.
 As Partes 
\begin_inset CommandInset ref
LatexCommand ref
reference "ch.TFL"
plural "false"
caps "false"
noprefix "false"

\end_inset

–
\begin_inset CommandInset ref
LatexCommand ref
reference "ch.NDTFL"
plural "false"
caps "false"
noprefix "false"

\end_inset

 ocupam-se com linguagens verofuncionais(TFL).
 Nelas sentenças são formadas a partir de sentenças básicas, usando-se alguns
 conectivos (`ou', `e', `não', `se \SpecialChar ldots
, então') que combinam justamente sentenças,
 formando sentenças mais complicadas.
 Discutimos noções lógicas tais como acarretamento [
\shape italic
entailment
\shape default
] em duas formas: semanticamente, usando o método de tabelas de verdade
 (na Parte
\begin_inset space ~
\end_inset


\begin_inset CommandInset ref
LatexCommand ref
reference "ch.TruthTables"
plural "false"
caps "false"
noprefix "false"

\end_inset

) e na teoria da prova, usando um sistema de derivações formais (na Parte
\begin_inset space ~
\end_inset


\begin_inset CommandInset ref
LatexCommand ref
reference "ch.NDTFL"
plural "false"
caps "false"
noprefix "false"

\end_inset

).
 As Partes 
\begin_inset CommandInset ref
LatexCommand ref
reference "ch.FOL"
plural "false"
caps "false"
noprefix "false"

\end_inset

–
\begin_inset CommandInset ref
LatexCommand ref
reference "ch.NDFOL"
plural "false"
caps "false"
noprefix "false"

\end_inset

 lidam com uma linguagem mais complicada, a da lógica de primeira ordem.
 Ela inclui, além dos conectivos da lógica verofuncional, também nomes,
 predicados, identidade e os então chamados quantificadores.
 Estes elementos adicionais da linguagem a tornam muito mais expressiva
 do que a linguagem verofuncional e passaremos uma grande quantidade de
 tempo investigando justamente o quanto se pode expressar nela.
 Novamente, noções lógicas para linguagem da lógica de primeira ordem são
 definidas semanticamente, usando-se interpretações, e na teoria da prova,
 usando-se uma versão mais complexa do sistema de derivação formal introduzida
 na Parte
\begin_inset space ~
\end_inset


\begin_inset CommandInset ref
LatexCommand ref
reference "ch.NDTFL"
plural "false"
caps "false"
noprefix "false"

\end_inset

.
 Parte
\begin_inset space ~
\end_inset


\begin_inset CommandInset ref
LatexCommand ref
reference "ch.ML"
plural "false"
caps "false"
noprefix "false"

\end_inset

 discute a extensão da TFL por meio de operadores não-verofuncionais para
 possibilidade e necessidade: lógica modal.
 Parte
\begin_inset space ~
\end_inset


\begin_inset CommandInset ref
LatexCommand ref
reference "ch.normalform"
plural "false"
caps "false"
noprefix "false"

\end_inset

 cobre dois tópicos avançados: o primeiro diz respeito às formas normais
 conjuntivas e disjuntivas e à adequação expressiva dos conectivos verofuncionai
s; o segundo diz respeito à corretude [
\shape italic
soundness
\shape default
] da dedução natural para TFL.
\end_layout

\begin_layout Standard
Nos apêndices, você encontrará uma discussão de notações alternativas para
 as linguagens que discutimos neste texto, discussão de sistemas alternativos
 de derivação e uma rápida referência que lista as regras e definições mais
 importantes.
 Os termos centrais são listados em um glossário no fim.
\end_layout

\begin_layout Standard
Este livro é baseado em um texto que foi originalmente escrito por P.
\begin_inset space ~
\end_inset

D.
 Magnus na versão revisada e expandida por Tim Button.
 Ele também inclui algum material de J.
\begin_inset space ~
\end_inset

Robert Loftis.
 O material na Parte
\begin_inset space ~
\end_inset


\begin_inset CommandInset ref
LatexCommand ref
reference "ch.ML"
plural "false"
caps "false"
noprefix "false"

\end_inset

 é baseado em notas de Robert Trueman e o material na Parte
\begin_inset space ~
\end_inset


\begin_inset CommandInset ref
LatexCommand ref
reference "ch.normalform"
plural "false"
caps "false"
noprefix "false"

\end_inset

 é baseado em dois capítulos do texto aberto 
\emph on
Metatheory
\emph default
 de Tim Button.
 Aaron Thomas-Bolduc e Richard Zach combinaram elementos destes textos na
 presente versão, mudaram algumas terminologias e alguns exemplos, reescreveram
 algumas seções e adicionaram material próprio.
 O texto resultante é licenciado sob uma licença Creative Commons Attribution
 4.0.
\end_layout

\begin_layout Standard

\end_layout

\end_body
\end_document
